M1, M2, M:MsgA. M1 || M2  M  M1  M  M1  M2 

latex

Definitions	MsgA, t  T, x:A. B(x), M1 || M2, P  Q, M1  M2, M1  M2, M1 ||decl M2, P & Q
Lemmas	ma-sub transitivity, ma-join wf, ma-sub-join-left, ma-sub wf, ma-compatible wf, msga wf